$\vdash$  $\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $i$, $u$:$T$. ($i$ = $u$) $\Rightarrow$ ($P$($u$)) $\Rightarrow$ ($i$ = $u$)